\begin{tabbing}
$M$.rframe($A$.effect $f$ of $k$ on $y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=IdIdDeq$\forall$$x$$\in$dom(($M$.2.2.2.2.2.2.2.2.2.2).1). \+
\\[0ex]
\\[0ex]$L$\==($M$.2.2.2.2.2.2.2.2.2.2).1($x$) $\Rightarrow$ \+
\\[0ex]($\uparrow$deq{-}member(KindDeq;$k$;$L$))
\-\\[0ex]$\vee$ \=($\forall$$s_{1}$:$A$.state, $s_{2}$:$A$.state, $v$:$A$.da($k$).\+
\\[0ex]ma{-}x{-}equiv($A$;$x$;$s_{1}$;$s_{2}$) $\Rightarrow$ ($f$($s_{1}$,$v$) = $f$($s_{2}$,$v$) $\in$ $\mathbb{Q}\rightarrow$fpf{-}cap($A$.1;IdDeq;$y$;Void)))
\-\-
\end{tabbing}